g:OGrp. (ghgrp)  OCMon 

latex

Up	groups 1
Definitions of Statement	|g|, =, , *, e, Mon, AbMon, IsMonHom{M1,M2}(f), IsMonHomInj(g;h;f), OCMon, OGrp, |g|, ghgrp
Definitions	t  T, x:A. B(x), x,y. t(x;y), , t.2, t.1, , =, x f y, P & Q, ghgrp, |g|, x:A. B(x), P  Q, e, *, FunThru2op(A;B;opa;opb;f), Inj(A;B;f), IsMonHom{M1,M2}(f), IsMonHomInj(g;h;f), |g|, P  Q, P  Q, RelsIso(T;T';x,y.R(x;y);x,y.R'(x;y);f), x(s1,s2), Mon, AbMon, OCMon, OGrp
Lemmas	ocgrp wf, hgrp of ocgrp wf, inj into ocmon, grp le wf, grp eq wf, assert wf, grp car wf, rels iso wf, mon hom inj p wf, hgrp car wf, grp id wf, grp op wf, grp leq wf, hgrp car properties